Iof proof for Lemma comb for pi2 wf:
(
A,B,p,z. p.2) 
A:Type
B:(AType)p:(a:A 
B(a))(
True)B(p.1)
by (ProveOpCombinatorTyping (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
)) (first_tok :t) inil_term)) `pi2_wf`
.| 9,38 |
(A,B,p,z. p.2) A:TypeB:(AType)p:(a:A B(a))(True)B(p.1)
by (ProveOpCombinatorTyping (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
)) (first_tok :t) inil_term)) `pi2_wf`
.
| Definitions | T  x:A. B(x)T |
| Lemmas |